Left Termination of the query pattern
balance(g,a)
w.r.t. the given Prolog program could successfully be proven:

(0) Obligation:

Clauses:

balance(T, TB) :- balance(T, -(I, []), -(.(','(TB, -(I, [])), X), X), -(Rest, []), -(Rest, [])).
balance(nil, -(X, X), -(A, B), -(A, B), -(.(','(nil, -(C, C)), T), T)).
balance(tree(L, V, R), -(IH, IT), -(.(','(tree(LB, VB, RB), -(A, D)), H), .(','(LB, -(A, .(VB, X))), .(','(RB, -(X, D)), T))), -(HR, TR), -(NH, NT)) :- ','(balance(L, -(IH, .(V, IT1)), -(H, T), -(HR1, TR1), -(NH, NT1)), balance(R, -(IT1, IT), -(HR1, TR1), -(HR, TR), -(NT1, NT))).

Query: balance(g,a)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="D: balance(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: balance(T1, T2), SCOPE: 1, CLAUSE: 0\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: balance(T5, -(X5, []), -(.(','(T7, -(X5, [])), X6), X6), -(X7, []), -(X7, []))\n\nT5 is ground\nX5 is free\nX6 is free\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: balance(T5, -(X5, []), -(.(','(T7, -(X5, [])), X6), X6), -(X7, []), -(X7, [])), SCOPE: 2, CLAUSE: 1 | balance(T5, -(X5, []), -(.(','(T7, -(X5, [])), X6), X6), -(X7, []), -(X7, [])), SCOPE: 2, CLAUSE: 2\n\nT5 is ground\nX5 is free\nX6 is free\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: balance(T5, -(X5, []), -(.(','(T7, -(X5, [])), X6), X6), -(X7, []), -(X7, [])), SCOPE: 2, CLAUSE: 1\n\nT5 is ground\nX5 is free\nX6 is free\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: balance(T5, -(X5, []), -(.(','(T7, -(X5, [])), X6), X6), -(X7, []), -(X7, [])), SCOPE: 2, CLAUSE: 2\n\nT5 is ground\nX5 is free\nX6 is free\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(balance(T25, -(T31, .(T26, X108)), -(.(','(T33, -(T31, .(T34, T35))), .(','(T36, -(T35, [])), T32)), T32), -(X109, X110), -(X116, X111)), balance(T27, -(X108, []), -(X109, X110), -(X116, []), -(X111, [])))\n\nT25 is ground\nT26 is ground\nT27 is ground\nX116 is free\nX108 is free\nX109 is free\nX110 is free\nX111 is free", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="C: balance(T25, -(T31, .(T26, X108)), -(.(','(T33, -(T31, .(T34, T35))), .(','(T36, -(T35, [])), T32)), T32), -(X109, X110), -(X116, X111))\n\nT25 is ground\nT26 is ground\nX116 is free\nX108 is free\nX109 is free\nX110 is free\nX111 is free", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="B: balance(T27, -(T53, []), -(T54, T55), -(T56, []), -(T57, []))\n\nT27 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: balance(T25, -(T31, .(T26, X108)), -(.(','(T33, -(T31, .(T34, T35))), .(','(T36, -(T35, [])), T32)), T32), -(X109, X110), -(X116, X111)), SCOPE: 3, CLAUSE: 1 | balance(T25, -(T31, .(T26, X108)), -(.(','(T33, -(T31, .(T34, T35))), .(','(T36, -(T35, [])), T32)), T32), -(X109, X110), -(X116, X111)), SCOPE: 3, CLAUSE: 2\n\nT25 is ground\nT26 is ground\nX116 is free\nX108 is free\nX109 is free\nX110 is free\nX111 is free", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: balance(T25, -(T31, .(T26, X108)), -(.(','(T33, -(T31, .(T34, T35))), .(','(T36, -(T35, [])), T32)), T32), -(X109, X110), -(X116, X111)), SCOPE: 3, CLAUSE: 1\n\nT25 is ground\nT26 is ground\nX116 is free\nX108 is free\nX109 is free\nX110 is free\nX111 is free", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: balance(T25, -(T31, .(T26, X108)), -(.(','(T33, -(T31, .(T34, T35))), .(','(T36, -(T35, [])), T32)), T32), -(X109, X110), -(X116, X111)), SCOPE: 3, CLAUSE: 2\n\nT25 is ground\nT26 is ground\nX116 is free\nX108 is free\nX109 is free\nX110 is free\nX111 is free", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: ','(balance(T142, -(T156, .(T143, X245)), -(.(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157), -(X246, X247), -(X252, X248)), balance(T144, -(X245, .(T146, X249)), -(X246, X247), -(X250, X251), -(X248, X253)))\n\nT142 is ground\nT143 is ground\nT144 is ground\nT146 is ground\nX249 is free\nX250 is free\nX251 is free\nX252 is free\nX253 is free\nX245 is free\nX246 is free\nX247 is free\nX248 is free", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: balance(T142, -(T156, .(T143, X245)), -(.(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))), T157), -(X246, X247), -(X252, X248))\n\nT142 is ground\nT143 is ground\nX252 is free\nX245 is free\nX246 is free\nX247 is free\nX248 is free", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="A: balance(T144, -(T187, .(T146, X249)), -(T188, T189), -(X250, X251), -(T191, X253))\n\nT144 is ground\nT146 is ground\nX249 is free\nX250 is free\nX251 is free\nX253 is free", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: balance(T144, -(T187, .(T146, X249)), -(T188, T189), -(X250, X251), -(T191, X253)), SCOPE: 4, CLAUSE: 1 | balance(T144, -(T187, .(T146, X249)), -(T188, T189), -(X250, X251), -(T191, X253)), SCOPE: 4, CLAUSE: 2\n\nT144 is ground\nT146 is ground\nX249 is free\nX250 is free\nX251 is free\nX253 is free", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: balance(T144, -(T187, .(T146, X249)), -(T188, T189), -(X250, X251), -(T191, X253)), SCOPE: 4, CLAUSE: 1\n\nT144 is ground\nT146 is ground\nX249 is free\nX250 is free\nX251 is free\nX253 is free", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: balance(T144, -(T187, .(T146, X249)), -(T188, T189), -(X250, X251), -(T191, X253)), SCOPE: 4, CLAUSE: 2\n\nT144 is ground\nT146 is ground\nX249 is free\nX250 is free\nX251 is free\nX253 is free", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: ','(balance(T291, -(T305, .(T292, X380)), -(T306, T307), -(X381, X382), -(T308, X383)), balance(T293, -(X380, .(T295, X384)), -(X381, X382), -(X385, X386), -(X383, X387)))\n\nT291 is ground\nT292 is ground\nT293 is ground\nT295 is ground\nX384 is free\nX385 is free\nX386 is free\nX387 is free\nX380 is free\nX381 is free\nX382 is free\nX383 is free", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: balance(T291, -(T305, .(T292, X380)), -(T306, T307), -(X381, X382), -(T308, X383))\n\nT291 is ground\nT292 is ground\nX380 is free\nX381 is free\nX382 is free\nX383 is free", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: balance(T293, -(T323, .(T295, X384)), -(T324, T325), -(X385, X386), -(T326, X387))\n\nT293 is ground\nT295 is ground\nX384 is free\nX385 is free\nX386 is free\nX387 is free", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: balance(T27, -(T53, []), -(T54, T55), -(T56, []), -(T57, [])), SCOPE: 5, CLAUSE: 1 | balance(T27, -(T53, []), -(T54, T55), -(T56, []), -(T57, [])), SCOPE: 5, CLAUSE: 2\n\nT27 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: balance(T27, -(T53, []), -(T54, T55), -(T56, []), -(T57, [])), SCOPE: 5, CLAUSE: 1\n\nT27 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: balance(T27, -(T53, []), -(T54, T55), -(T56, []), -(T57, [])), SCOPE: 5, CLAUSE: 2\n\nT27 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: ','(balance(T418, -(T432, .(T419, X508)), -(T433, T434), -(X509, X510), -(T435, X511)), balance(T420, -(X508, []), -(X509, X510), -(T436, []), -(X511, [])))\n\nT418 is ground\nT419 is ground\nT420 is ground\nX508 is free\nX509 is free\nX510 is free\nX511 is free", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: balance(T418, -(T432, .(T419, X508)), -(T433, T434), -(X509, X510), -(T435, X511))\n\nT418 is ground\nT419 is ground\nX508 is free\nX509 is free\nX510 is free\nX511 is free", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: balance(T420, -(T451, []), -(T452, T453), -(T455, []), -(T454, []))\n\nT420 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 44 [arrowhead = none ];
44 -> 2;

45 [label="ONLY EVAL with clause\nbalance(X3, X4) :- balance(X3, -(X5, []), -(.(','(X4, -(X5, [])), X6), X6), -(X7, []), -(X7, [])).\nand substitutionT1 -> T5,\nX3 -> T5,\nT2 -> T7,\nX4 -> T7,\nT6 -> T7", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 45 [arrowhead = none ];
45 -> 3;

46 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 46 [arrowhead = none ];
46 -> 4;

47 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
4 -> 47 [arrowhead = none ];
47 -> 5;

48 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
4 -> 48 [arrowhead = none ];
48 -> 6;

49 [label="EVAL with clause\nbalance(nil, -(X36, X36), -(X37, X38), -(X37, X38), -(.(','(nil, -(X39, X39)), X40), X40)).\nand substitutionT5 -> nil,\nX5 -> [],\nX36 -> [],\nX41 -> [],\nT7 -> nil,\nX6 -> [],\nX37 -> .(','(nil, -([], [])), []),\nX38 -> [],\nX7 -> .(','(nil, -([], [])), []),\nX42 -> [],\nT12 -> nil,\nX39 -> [],\nX40 -> []", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 49 [arrowhead = none ];
49 -> 7;

50 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
5 -> 50 [arrowhead = none ];
50 -> 8;

51 [label="EVAL with clause\nbalance(tree(X91, X92, X93), -(X94, X95), -(.(','(tree(X96, X97, X98), -(X99, X100)), X101), .(','(X96, -(X99, .(X97, X102))), .(','(X98, -(X102, X100)), X103))), -(X104, X105), -(X106, X107)) :- ','(balance(X91, -(X94, .(X92, X108)), -(X101, X103), -(X109, X110), -(X106, X111)), balance(X93, -(X108, X95), -(X109, X110), -(X104, X105), -(X111, X107))).\nand substitutionX91 -> T25,\nX92 -> T26,\nX93 -> T27,\nT5 -> tree(T25, T26, T27),\nX5 -> T31,\nX94 -> T31,\nX95 -> [],\nX96 -> T33,\nX97 -> T34,\nX98 -> T36,\nT7 -> tree(T33, T34, T36),\nX99 -> T31,\nX100 -> [],\nX6 -> .(','(T33, -(T31, .(T34, T35))), .(','(T36, -(T35, [])), T32)),\nX101 -> .(','(T33, -(T31, .(T34, T35))), .(','(T36, -(T35, [])), T32)),\nX102 -> T35,\nX103 -> T32,\nX113 -> .(','(T33, -(T31, .(T34, T35))), .(','(T36, -(T35, [])), T32)),\nX7 -> X116,\nX104 -> X116,\nX105 -> [],\nX106 -> X116,\nX107 -> [],\nX112 -> T31,\nX115 -> T32,\nT28 -> T33,\nT29 -> T34,\nX114 -> T35,\nT30 -> T36", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 51 [arrowhead = none ];
51 -> 10;

52 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
6 -> 52 [arrowhead = none ];
52 -> 11;

53 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
7 -> 53 [arrowhead = none ];
53 -> 9;

54 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
10 -> 54 [arrowhead = none ];
54 -> 12;

55 [label="SPLIT 2\nnew knowledge:\nT25 is ground\nreplacements:X108 -> T53,\nX109 -> T54,\nX110 -> T55,\nX116 -> T56,\nX111 -> T57", fontsize=14, style = filled, fillcolor = violet];
10 -> 55 [arrowhead = none ];
55 -> 13;

56 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
12 -> 56 [arrowhead = none ];
56 -> 14;

57 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
13 -> 57 [arrowhead = none ];
57 -> 34;

58 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
14 -> 58 [arrowhead = none ];
58 -> 15;

59 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
14 -> 59 [arrowhead = none ];
59 -> 16;

60 [label="EVAL with clause\nbalance(nil, -(X173, X173), -(X174, X175), -(X174, X175), -(.(','(nil, -(X176, X176)), X177), X177)).\nand substitutionT25 -> nil,\nT31 -> .(T107, T108),\nX173 -> .(T107, T108),\nT26 -> T107,\nX108 -> T108,\nT106 -> .(T107, T108),\nT33 -> T109,\nT34 -> T110,\nT35 -> T111,\nT36 -> T112,\nT32 -> T113,\nX174 -> .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)),\nX175 -> T113,\nX109 -> .(','(T109, -(.(T107, T108), .(T110, T111))), .(','(T112, -(T111, [])), T113)),\nX110 -> T113,\nX176 -> X178,\nX177 -> X179,\nX116 -> .(','(nil, -(X178, X178)), X179),\nX111 -> X179", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 60 [arrowhead = none ];
60 -> 17;

61 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
15 -> 61 [arrowhead = none ];
61 -> 18;

62 [label="EVAL with clause\nbalance(tree(X228, X229, X230), -(X231, X232), -(.(','(tree(X233, X234, X235), -(X236, X237)), X238), .(','(X233, -(X236, .(X234, X239))), .(','(X235, -(X239, X237)), X240))), -(X241, X242), -(X243, X244)) :- ','(balance(X228, -(X231, .(X229, X245)), -(X238, X240), -(X246, X247), -(X243, X248)), balance(X230, -(X245, X232), -(X246, X247), -(X241, X242), -(X248, X244))).\nand substitutionX228 -> T142,\nX229 -> T143,\nX230 -> T144,\nT25 -> tree(T142, T143, T144),\nT31 -> T156,\nX231 -> T156,\nT26 -> T146,\nX108 -> X249,\nX232 -> .(T146, X249),\nX233 -> T160,\nX234 -> T161,\nX235 -> T163,\nT33 -> tree(T160, T161, T163),\nX236 -> T156,\nT34 -> T164,\nT35 -> T159,\nX237 -> .(T164, T159),\nT36 -> T158,\nT32 -> .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)),\nX238 -> .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157))),\nX239 -> T162,\nX240 -> T157,\nT153 -> .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)),\nX109 -> X250,\nX241 -> X250,\nX110 -> X251,\nX242 -> X251,\nX116 -> X252,\nX243 -> X252,\nX111 -> X253,\nX244 -> X253,\nT145 -> T156,\nT155 -> T157,\nT152 -> T158,\nT151 -> T159,\nT147 -> T160,\nT148 -> T161,\nT154 -> T162,\nT149 -> T163,\nT150 -> T164", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 62 [arrowhead = none ];
62 -> 20;

63 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
16 -> 63 [arrowhead = none ];
63 -> 21;

64 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
17 -> 64 [arrowhead = none ];
64 -> 19;

65 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
20 -> 65 [arrowhead = none ];
65 -> 22;

66 [label="SPLIT 2\nnew knowledge:\nT142 is ground\nreplacements:X245 -> T187,\nX246 -> T188,\nX247 -> T189,\nX252 -> T190,\nX248 -> T191", fontsize=14, style = filled, fillcolor = violet];
20 -> 66 [arrowhead = none ];
66 -> 23;

67 [label="INSTANCE with matching:\nT144 -> T142\nT187 -> T156\nT146 -> T143\nX249 -> X245\nT188 -> .(','(T158, -(T159, [])), .(','(T160, -(T156, .(T161, T162))), .(','(T163, -(T162, .(T164, T159))), T157)))\nT189 -> T157\nX250 -> X246\nX251 -> X247\nT191 -> X252\nX253 -> X248", fontsize=14, style = filled, fillcolor = lightgrey];
22 -> 67 [arrowhead = none , style=dashed];
67 -> 23[style=dashed];

68 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
23 -> 68 [arrowhead = none ];
68 -> 24;

69 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
24 -> 69 [arrowhead = none ];
69 -> 25;

70 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
24 -> 70 [arrowhead = none ];
70 -> 26;

71 [label="EVAL with clause\nbalance(nil, -(X312, X312), -(X313, X314), -(X313, X314), -(.(','(nil, -(X315, X315)), X316), X316)).\nand substitutionT144 -> nil,\nT187 -> .(T257, T258),\nX312 -> .(T257, T258),\nT146 -> T257,\nX249 -> T258,\nT256 -> .(T257, T258),\nT188 -> T259,\nX313 -> T259,\nT189 -> T260,\nX314 -> T260,\nX250 -> T259,\nX251 -> T260,\nX315 -> T261,\nX316 -> T262,\nT191 -> .(','(nil, -(T261, T261)), T262),\nX253 -> T262", fontsize=14, style = filled, fillcolor = lightblue];
25 -> 71 [arrowhead = none ];
71 -> 27;

72 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
25 -> 72 [arrowhead = none ];
72 -> 28;

73 [label="EVAL with clause\nbalance(tree(X363, X364, X365), -(X366, X367), -(.(','(tree(X368, X369, X370), -(X371, X372)), X373), .(','(X368, -(X371, .(X369, X374))), .(','(X370, -(X374, X372)), X375))), -(X376, X377), -(X378, X379)) :- ','(balance(X363, -(X366, .(X364, X380)), -(X373, X375), -(X381, X382), -(X378, X383)), balance(X365, -(X380, X367), -(X381, X382), -(X376, X377), -(X383, X379))).\nand substitutionX363 -> T291,\nX364 -> T292,\nX365 -> T293,\nT144 -> tree(T291, T292, T293),\nT187 -> T305,\nX366 -> T305,\nT146 -> T295,\nX249 -> X384,\nX367 -> .(T295, X384),\nX368 -> T296,\nX369 -> T297,\nX370 -> T298,\nX371 -> T299,\nX372 -> T300,\nX373 -> T306,\nT188 -> .(','(tree(T296, T297, T298), -(T299, T300)), T306),\nX374 -> T302,\nX375 -> T307,\nT189 -> .(','(T296, -(T299, .(T297, T302))), .(','(T298, -(T302, T300)), T307)),\nX250 -> X385,\nX376 -> X385,\nX251 -> X386,\nX377 -> X386,\nT191 -> T308,\nX378 -> T308,\nX253 -> X387,\nX379 -> X387,\nT294 -> T305,\nT301 -> T306,\nT303 -> T307,\nT304 -> T308", fontsize=14, style = filled, fillcolor = lightblue];
26 -> 73 [arrowhead = none ];
73 -> 30;

74 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
26 -> 74 [arrowhead = none ];
74 -> 31;

75 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
27 -> 75 [arrowhead = none ];
75 -> 29;

76 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
30 -> 76 [arrowhead = none ];
76 -> 32;

77 [label="SPLIT 2\nnew knowledge:\nT291 is ground\nreplacements:X380 -> T323,\nX381 -> T324,\nX382 -> T325,\nX383 -> T326", fontsize=14, style = filled, fillcolor = violet];
30 -> 77 [arrowhead = none ];
77 -> 33;

78 [label="INSTANCE with matching:\nT144 -> T291\nT187 -> T305\nT146 -> T292\nX249 -> X380\nT188 -> T306\nT189 -> T307\nX250 -> X381\nX251 -> X382\nT191 -> T308\nX253 -> X383", fontsize=14, style = filled, fillcolor = lightgrey];
32 -> 78 [arrowhead = none , style=dashed];
78 -> 23[style=dashed];

79 [label="INSTANCE with matching:\nT144 -> T293\nT187 -> T323\nT146 -> T295\nX249 -> X384\nT188 -> T324\nT189 -> T325\nX250 -> X385\nX251 -> X386\nT191 -> T326\nX253 -> X387", fontsize=14, style = filled, fillcolor = lightgrey];
33 -> 79 [arrowhead = none , style=dashed];
79 -> 23[style=dashed];

80 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
34 -> 80 [arrowhead = none ];
80 -> 35;

81 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
34 -> 81 [arrowhead = none ];
81 -> 36;

82 [label="EVAL with clause\nbalance(nil, -(X448, X448), -(X449, X450), -(X449, X450), -(.(','(nil, -(X451, X451)), X452), X452)).\nand substitutionT27 -> nil,\nT53 -> [],\nX448 -> [],\nT385 -> [],\nT54 -> T386,\nX449 -> T386,\nT55 -> [],\nX450 -> [],\nT56 -> T386,\nT387 -> [],\nX451 -> T388,\nX452 -> [],\nT57 -> .(','(nil, -(T388, T388)), []),\nT389 -> []", fontsize=14, style = filled, fillcolor = lightblue];
35 -> 82 [arrowhead = none ];
82 -> 37;

83 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
35 -> 83 [arrowhead = none ];
83 -> 38;

84 [label="EVAL with clause\nbalance(tree(X491, X492, X493), -(X494, X495), -(.(','(tree(X496, X497, X498), -(X499, X500)), X501), .(','(X496, -(X499, .(X497, X502))), .(','(X498, -(X502, X500)), X503))), -(X504, X505), -(X506, X507)) :- ','(balance(X491, -(X494, .(X492, X508)), -(X501, X503), -(X509, X510), -(X506, X511)), balance(X493, -(X508, X495), -(X509, X510), -(X504, X505), -(X511, X507))).\nand substitutionX491 -> T418,\nX492 -> T419,\nX493 -> T420,\nT27 -> tree(T418, T419, T420),\nT53 -> T432,\nX494 -> T432,\nX495 -> [],\nX496 -> T422,\nX497 -> T423,\nX498 -> T424,\nX499 -> T425,\nX500 -> T426,\nX501 -> T433,\nT54 -> .(','(tree(T422, T423, T424), -(T425, T426)), T433),\nX502 -> T428,\nX503 -> T434,\nT55 -> .(','(T422, -(T425, .(T423, T428))), .(','(T424, -(T428, T426)), T434)),\nT56 -> T436,\nX504 -> T436,\nX505 -> [],\nT57 -> T435,\nX506 -> T435,\nX507 -> [],\nT421 -> T432,\nT427 -> T433,\nT429 -> T434,\nT431 -> T435,\nT430 -> T436", fontsize=14, style = filled, fillcolor = lightblue];
36 -> 84 [arrowhead = none ];
84 -> 40;

85 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
36 -> 85 [arrowhead = none ];
85 -> 41;

86 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
37 -> 86 [arrowhead = none ];
86 -> 39;

87 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
40 -> 87 [arrowhead = none ];
87 -> 42;

88 [label="SPLIT 2\nnew knowledge:\nT418 is ground\nreplacements:X508 -> T451,\nX509 -> T452,\nX510 -> T453,\nX511 -> T454,\nT436 -> T455", fontsize=14, style = filled, fillcolor = violet];
40 -> 88 [arrowhead = none ];
88 -> 43;

89 [label="INSTANCE with matching:\nT144 -> T418\nT187 -> T432\nT146 -> T419\nX249 -> X508\nT188 -> T433\nT189 -> T434\nX250 -> X509\nX251 -> X510\nT191 -> T435\nX253 -> X511", fontsize=14, style = filled, fillcolor = lightgrey];
42 -> 89 [arrowhead = none , style=dashed];
89 -> 23[style=dashed];

90 [label="INSTANCE with matching:\nT27 -> T420\nT53 -> T451\nT54 -> T452\nT55 -> T453\nT56 -> T455\nT57 -> T454", fontsize=14, style = filled, fillcolor = lightgrey];
43 -> 90 [arrowhead = none , style=dashed];
90 -> 13[style=dashed];

}

(2) Obligation:

Triples:

balanceA(tree(X1, X2, X3), X4, X5, X6, .(','(tree(X7, X8, X9), -(X10, X11)), X12), .(','(X7, -(X10, .(X8, X13))), .(','(X9, -(X13, X11)), X14)), X15, X16, X17, X18) :- balanceA(X1, X4, X2, X19, X12, X14, X20, X21, X17, X22).
balanceA(tree(X1, X2, X3), X4, X5, X6, .(','(tree(X7, X8, X9), -(X10, X11)), X12), .(','(X7, -(X10, .(X8, X13))), .(','(X9, -(X13, X11)), X14)), X15, X16, X17, X18) :- ','(balancecA(X1, X4, X2, X19, X12, X14, X20, X21, X17, X22), balanceA(X3, X19, X5, X6, X20, X21, X15, X16, X22, X18)).
balanceB(tree(X1, X2, X3), X4, .(','(tree(X5, X6, X7), -(X8, X9)), X10), .(','(X5, -(X8, .(X6, X11))), .(','(X7, -(X11, X9)), X12)), X13, X14) :- balanceA(X1, X4, X2, X15, X10, X12, X16, X17, X14, X18).
balanceB(tree(X1, X2, X3), X4, .(','(tree(X5, X6, X7), -(X8, X9)), X10), .(','(X5, -(X8, .(X6, X11))), .(','(X7, -(X11, X9)), X12)), X13, X14) :- ','(balancecA(X1, X4, X2, X15, X10, X12, X16, X17, X14, X18), balanceB(X3, X15, X16, X17, X13, X18)).
balanceD(tree(tree(X1, X2, X3), X4, X5), tree(tree(X6, X7, X8), X9, X10)) :- balanceA(X1, X11, X2, X12, .(','(X10, -(X13, [])), .(','(X6, -(X11, .(X7, X14))), .(','(X8, -(X14, .(X9, X13))), X15))), X15, X16, X17, X18, X19).
balanceD(tree(tree(X1, X2, X3), X4, X5), tree(tree(X6, X7, X8), X9, X10)) :- ','(balancecA(X1, X11, X2, X12, .(','(X10, -(X13, [])), .(','(X6, -(X11, .(X7, X14))), .(','(X8, -(X14, .(X9, X13))), X15))), X15, X16, X17, X18, X19), balanceA(X3, X12, X4, X20, X16, X17, X21, X22, X19, X23)).
balanceD(tree(X1, X2, X3), tree(X4, X5, X6)) :- ','(balancecC(X1, X7, X2, X8, X4, X5, X9, X6, X10, X11, X12, X13, X14), balanceB(X3, X8, X11, X12, X13, X14)).

Clauses:

balancecA(nil, .(X1, X2), X1, X2, X3, X4, X3, X4, .(','(nil, -(X5, X5)), X6), X6).
balancecA(tree(X1, X2, X3), X4, X5, X6, .(','(tree(X7, X8, X9), -(X10, X11)), X12), .(','(X7, -(X10, .(X8, X13))), .(','(X9, -(X13, X11)), X14)), X15, X16, X17, X18) :- ','(balancecA(X1, X4, X2, X19, X12, X14, X20, X21, X17, X22), balancecA(X3, X19, X5, X6, X20, X21, X15, X16, X22, X18)).
balancecB(nil, [], X1, [], X1, .(','(nil, -(X2, X2)), [])).
balancecB(tree(X1, X2, X3), X4, .(','(tree(X5, X6, X7), -(X8, X9)), X10), .(','(X5, -(X8, .(X6, X11))), .(','(X7, -(X11, X9)), X12)), X13, X14) :- ','(balancecA(X1, X4, X2, X15, X10, X12, X16, X17, X14, X18), balancecB(X3, X15, X16, X17, X13, X18)).
balancecC(nil, .(X1, X2), X1, X2, X3, X4, X5, X6, X7, .(','(X3, -(.(X1, X2), .(X4, X5))), .(','(X6, -(X5, [])), X7)), X7, .(','(nil, -(X8, X8)), X9), X9).
balancecC(tree(X1, X2, X3), X4, X5, X6, tree(X7, X8, X9), X10, X11, X12, .(','(X7, -(X4, .(X8, X13))), .(','(X9, -(X13, .(X10, X11))), X14)), X15, X16, X17, X18) :- ','(balancecA(X1, X4, X2, X19, .(','(X12, -(X11, [])), .(','(X7, -(X4, .(X8, X13))), .(','(X9, -(X13, .(X10, X11))), X14))), X14, X20, X21, X17, X22), balancecA(X3, X19, X5, X6, X20, X21, X15, X16, X22, X18)).

Afs:

balanceD(x1, x2)  =  balanceD(x1)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
balanceD_in: (b,f)
balanceA_in: (b,f,b,f,f,f,f,f,f,f)
balancecA_in: (b,f,b,f,f,f,f,f,f,f)
balancecC_in: (b,f,b,f,f,f,f,f,f,f,f,f,f)
balanceB_in: (b,f,f,f,f,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

BALANCED_IN_GA(tree(tree(X1, X2, X3), X4, X5), tree(tree(X6, X7, X8), X9, X10)) → U7_GA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, balanceA_in_gagaaaaaaa(X1, X11, X2, X12, .(','(X10, -(X13, [])), .(','(X6, -(X11, .(X7, X14))), .(','(X8, -(X14, .(X9, X13))), X15))), X15, X16, X17, X18, X19))
BALANCED_IN_GA(tree(tree(X1, X2, X3), X4, X5), tree(tree(X6, X7, X8), X9, X10)) → BALANCEA_IN_GAGAAAAAAA(X1, X11, X2, X12, .(','(X10, -(X13, [])), .(','(X6, -(X11, .(X7, X14))), .(','(X8, -(X14, .(X9, X13))), X15))), X15, X16, X17, X18, X19)
BALANCEA_IN_GAGAAAAAAA(tree(X1, X2, X3), X4, X5, X6, .(','(tree(X7, X8, X9), -(X10, X11)), X12), .(','(X7, -(X10, .(X8, X13))), .(','(X9, -(X13, X11)), X14)), X15, X16, X17, X18) → U1_GAGAAAAAAA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, balanceA_in_gagaaaaaaa(X1, X4, X2, X19, X12, X14, X20, X21, X17, X22))
BALANCEA_IN_GAGAAAAAAA(tree(X1, X2, X3), X4, X5, X6, .(','(tree(X7, X8, X9), -(X10, X11)), X12), .(','(X7, -(X10, .(X8, X13))), .(','(X9, -(X13, X11)), X14)), X15, X16, X17, X18) → BALANCEA_IN_GAGAAAAAAA(X1, X4, X2, X19, X12, X14, X20, X21, X17, X22)
BALANCEA_IN_GAGAAAAAAA(tree(X1, X2, X3), X4, X5, X6, .(','(tree(X7, X8, X9), -(X10, X11)), X12), .(','(X7, -(X10, .(X8, X13))), .(','(X9, -(X13, X11)), X14)), X15, X16, X17, X18) → U2_GAGAAAAAAA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, balancecA_in_gagaaaaaaa(X1, X4, X2, X19, X12, X14, X20, X21, X17, X22))
U2_GAGAAAAAAA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, balancecA_out_gagaaaaaaa(X1, X4, X2, X19, X12, X14, X20, X21, X17, X22)) → U3_GAGAAAAAAA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, balanceA_in_gagaaaaaaa(X3, X19, X5, X6, X20, X21, X15, X16, X22, X18))
U2_GAGAAAAAAA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, balancecA_out_gagaaaaaaa(X1, X4, X2, X19, X12, X14, X20, X21, X17, X22)) → BALANCEA_IN_GAGAAAAAAA(X3, X19, X5, X6, X20, X21, X15, X16, X22, X18)
BALANCED_IN_GA(tree(tree(X1, X2, X3), X4, X5), tree(tree(X6, X7, X8), X9, X10)) → U8_GA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, balancecA_in_gagaaaaaaa(X1, X11, X2, X12, .(','(X10, -(X13, [])), .(','(X6, -(X11, .(X7, X14))), .(','(X8, -(X14, .(X9, X13))), X15))), X15, X16, X17, X18, X19))
U8_GA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, balancecA_out_gagaaaaaaa(X1, X11, X2, X12, .(','(X10, -(X13, [])), .(','(X6, -(X11, .(X7, X14))), .(','(X8, -(X14, .(X9, X13))), X15))), X15, X16, X17, X18, X19)) → U9_GA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, balanceA_in_gagaaaaaaa(X3, X12, X4, X20, X16, X17, X21, X22, X19, X23))
U8_GA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, balancecA_out_gagaaaaaaa(X1, X11, X2, X12, .(','(X10, -(X13, [])), .(','(X6, -(X11, .(X7, X14))), .(','(X8, -(X14, .(X9, X13))), X15))), X15, X16, X17, X18, X19)) → BALANCEA_IN_GAGAAAAAAA(X3, X12, X4, X20, X16, X17, X21, X22, X19, X23)
BALANCED_IN_GA(tree(X1, X2, X3), tree(X4, X5, X6)) → U10_GA(X1, X2, X3, X4, X5, X6, balancecC_in_gagaaaaaaaaaa(X1, X7, X2, X8, X4, X5, X9, X6, X10, X11, X12, X13, X14))
U10_GA(X1, X2, X3, X4, X5, X6, balancecC_out_gagaaaaaaaaaa(X1, X7, X2, X8, X4, X5, X9, X6, X10, X11, X12, X13, X14)) → U11_GA(X1, X2, X3, X4, X5, X6, balanceB_in_gaaaaa(X3, X8, X11, X12, X13, X14))
U10_GA(X1, X2, X3, X4, X5, X6, balancecC_out_gagaaaaaaaaaa(X1, X7, X2, X8, X4, X5, X9, X6, X10, X11, X12, X13, X14)) → BALANCEB_IN_GAAAAA(X3, X8, X11, X12, X13, X14)
BALANCEB_IN_GAAAAA(tree(X1, X2, X3), X4, .(','(tree(X5, X6, X7), -(X8, X9)), X10), .(','(X5, -(X8, .(X6, X11))), .(','(X7, -(X11, X9)), X12)), X13, X14) → U4_GAAAAA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, balanceA_in_gagaaaaaaa(X1, X4, X2, X15, X10, X12, X16, X17, X14, X18))
BALANCEB_IN_GAAAAA(tree(X1, X2, X3), X4, .(','(tree(X5, X6, X7), -(X8, X9)), X10), .(','(X5, -(X8, .(X6, X11))), .(','(X7, -(X11, X9)), X12)), X13, X14) → BALANCEA_IN_GAGAAAAAAA(X1, X4, X2, X15, X10, X12, X16, X17, X14, X18)
BALANCEB_IN_GAAAAA(tree(X1, X2, X3), X4, .(','(tree(X5, X6, X7), -(X8, X9)), X10), .(','(X5, -(X8, .(X6, X11))), .(','(X7, -(X11, X9)), X12)), X13, X14) → U5_GAAAAA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, balancecA_in_gagaaaaaaa(X1, X4, X2, X15, X10, X12, X16, X17, X14, X18))
U5_GAAAAA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, balancecA_out_gagaaaaaaa(X1, X4, X2, X15, X10, X12, X16, X17, X14, X18)) → U6_GAAAAA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, balanceB_in_gaaaaa(X3, X15, X16, X17, X13, X18))
U5_GAAAAA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, balancecA_out_gagaaaaaaa(X1, X4, X2, X15, X10, X12, X16, X17, X14, X18)) → BALANCEB_IN_GAAAAA(X3, X15, X16, X17, X13, X18)

The TRS R consists of the following rules:

balancecA_in_gagaaaaaaa(nil, .(X1, X2), X1, X2, X3, X4, X3, X4, .(','(nil, -(X5, X5)), X6), X6) → balancecA_out_gagaaaaaaa(nil, .(X1, X2), X1, X2, X3, X4, X3, X4, .(','(nil, -(X5, X5)), X6), X6)
balancecA_in_gagaaaaaaa(tree(X1, X2, X3), X4, X5, X6, .(','(tree(X7, X8, X9), -(X10, X11)), X12), .(','(X7, -(X10, .(X8, X13))), .(','(X9, -(X13, X11)), X14)), X15, X16, X17, X18) → U13_gagaaaaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, balancecA_in_gagaaaaaaa(X1, X4, X2, X19, X12, X14, X20, X21, X17, X22))
U13_gagaaaaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, balancecA_out_gagaaaaaaa(X1, X4, X2, X19, X12, X14, X20, X21, X17, X22)) → U14_gagaaaaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, balancecA_in_gagaaaaaaa(X3, X19, X5, X6, X20, X21, X15, X16, X22, X18))
U14_gagaaaaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, balancecA_out_gagaaaaaaa(X3, X19, X5, X6, X20, X21, X15, X16, X22, X18)) → balancecA_out_gagaaaaaaa(tree(X1, X2, X3), X4, X5, X6, .(','(tree(X7, X8, X9), -(X10, X11)), X12), .(','(X7, -(X10, .(X8, X13))), .(','(X9, -(X13, X11)), X14)), X15, X16, X17, X18)
balancecC_in_gagaaaaaaaaaa(nil, .(X1, X2), X1, X2, X3, X4, X5, X6, X7, .(','(X3, -(.(X1, X2), .(X4, X5))), .(','(X6, -(X5, [])), X7)), X7, .(','(nil, -(X8, X8)), X9), X9) → balancecC_out_gagaaaaaaaaaa(nil, .(X1, X2), X1, X2, X3, X4, X5, X6, X7, .(','(X3, -(.(X1, X2), .(X4, X5))), .(','(X6, -(X5, [])), X7)), X7, .(','(nil, -(X8, X8)), X9), X9)
balancecC_in_gagaaaaaaaaaa(tree(X1, X2, X3), X4, X5, X6, tree(X7, X8, X9), X10, X11, X12, .(','(X7, -(X4, .(X8, X13))), .(','(X9, -(X13, .(X10, X11))), X14)), X15, X16, X17, X18) → U17_gagaaaaaaaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, balancecA_in_gagaaaaaaa(X1, X4, X2, X19, .(','(X12, -(X11, [])), .(','(X7, -(X4, .(X8, X13))), .(','(X9, -(X13, .(X10, X11))), X14))), X14, X20, X21, X17, X22))
U17_gagaaaaaaaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, balancecA_out_gagaaaaaaa(X1, X4, X2, X19, .(','(X12, -(X11, [])), .(','(X7, -(X4, .(X8, X13))), .(','(X9, -(X13, .(X10, X11))), X14))), X14, X20, X21, X17, X22)) → U18_gagaaaaaaaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, balancecA_in_gagaaaaaaa(X3, X19, X5, X6, X20, X21, X15, X16, X22, X18))
U18_gagaaaaaaaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, balancecA_out_gagaaaaaaa(X3, X19, X5, X6, X20, X21, X15, X16, X22, X18)) → balancecC_out_gagaaaaaaaaaa(tree(X1, X2, X3), X4, X5, X6, tree(X7, X8, X9), X10, X11, X12, .(','(X7, -(X4, .(X8, X13))), .(','(X9, -(X13, .(X10, X11))), X14)), X15, X16, X17, X18)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
balanceA_in_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balanceA_in_gagaaaaaaa(x1, x3)
balancecA_in_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balancecA_in_gagaaaaaaa(x1, x3)
nil  =  nil
balancecA_out_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balancecA_out_gagaaaaaaa(x1, x3)
U13_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U13_gagaaaaaaa(x1, x2, x3, x5, x19)
U14_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23)  =  U14_gagaaaaaaa(x1, x2, x3, x5, x23)
balancecC_in_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  balancecC_in_gagaaaaaaaaaa(x1, x3)
balancecC_out_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  balancecC_out_gagaaaaaaaaaa(x1, x3)
U17_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U17_gagaaaaaaaaaa(x1, x2, x3, x5, x19)
U18_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23)  =  U18_gagaaaaaaaaaa(x1, x2, x3, x5, x23)
balanceB_in_gaaaaa(x1, x2, x3, x4, x5, x6)  =  balanceB_in_gaaaaa(x1)
BALANCED_IN_GA(x1, x2)  =  BALANCED_IN_GA(x1)
U7_GA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U7_GA(x1, x2, x3, x4, x5, x11)
BALANCEA_IN_GAGAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  BALANCEA_IN_GAGAAAAAAA(x1, x3)
U1_GAGAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U1_GAGAAAAAAA(x1, x2, x3, x5, x19)
U2_GAGAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U2_GAGAAAAAAA(x1, x2, x3, x5, x19)
U3_GAGAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U3_GAGAAAAAAA(x1, x2, x3, x5, x19)
U8_GA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U8_GA(x1, x2, x3, x4, x5, x11)
U9_GA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U9_GA(x1, x2, x3, x4, x5, x11)
U10_GA(x1, x2, x3, x4, x5, x6, x7)  =  U10_GA(x1, x2, x3, x7)
U11_GA(x1, x2, x3, x4, x5, x6, x7)  =  U11_GA(x1, x2, x3, x7)
BALANCEB_IN_GAAAAA(x1, x2, x3, x4, x5, x6)  =  BALANCEB_IN_GAAAAA(x1)
U4_GAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)  =  U4_GAAAAA(x1, x2, x3, x15)
U5_GAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)  =  U5_GAAAAA(x1, x2, x3, x15)
U6_GAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)  =  U6_GAAAAA(x1, x2, x3, x15)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

BALANCED_IN_GA(tree(tree(X1, X2, X3), X4, X5), tree(tree(X6, X7, X8), X9, X10)) → U7_GA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, balanceA_in_gagaaaaaaa(X1, X11, X2, X12, .(','(X10, -(X13, [])), .(','(X6, -(X11, .(X7, X14))), .(','(X8, -(X14, .(X9, X13))), X15))), X15, X16, X17, X18, X19))
BALANCED_IN_GA(tree(tree(X1, X2, X3), X4, X5), tree(tree(X6, X7, X8), X9, X10)) → BALANCEA_IN_GAGAAAAAAA(X1, X11, X2, X12, .(','(X10, -(X13, [])), .(','(X6, -(X11, .(X7, X14))), .(','(X8, -(X14, .(X9, X13))), X15))), X15, X16, X17, X18, X19)
BALANCEA_IN_GAGAAAAAAA(tree(X1, X2, X3), X4, X5, X6, .(','(tree(X7, X8, X9), -(X10, X11)), X12), .(','(X7, -(X10, .(X8, X13))), .(','(X9, -(X13, X11)), X14)), X15, X16, X17, X18) → U1_GAGAAAAAAA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, balanceA_in_gagaaaaaaa(X1, X4, X2, X19, X12, X14, X20, X21, X17, X22))
BALANCEA_IN_GAGAAAAAAA(tree(X1, X2, X3), X4, X5, X6, .(','(tree(X7, X8, X9), -(X10, X11)), X12), .(','(X7, -(X10, .(X8, X13))), .(','(X9, -(X13, X11)), X14)), X15, X16, X17, X18) → BALANCEA_IN_GAGAAAAAAA(X1, X4, X2, X19, X12, X14, X20, X21, X17, X22)
BALANCEA_IN_GAGAAAAAAA(tree(X1, X2, X3), X4, X5, X6, .(','(tree(X7, X8, X9), -(X10, X11)), X12), .(','(X7, -(X10, .(X8, X13))), .(','(X9, -(X13, X11)), X14)), X15, X16, X17, X18) → U2_GAGAAAAAAA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, balancecA_in_gagaaaaaaa(X1, X4, X2, X19, X12, X14, X20, X21, X17, X22))
U2_GAGAAAAAAA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, balancecA_out_gagaaaaaaa(X1, X4, X2, X19, X12, X14, X20, X21, X17, X22)) → U3_GAGAAAAAAA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, balanceA_in_gagaaaaaaa(X3, X19, X5, X6, X20, X21, X15, X16, X22, X18))
U2_GAGAAAAAAA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, balancecA_out_gagaaaaaaa(X1, X4, X2, X19, X12, X14, X20, X21, X17, X22)) → BALANCEA_IN_GAGAAAAAAA(X3, X19, X5, X6, X20, X21, X15, X16, X22, X18)
BALANCED_IN_GA(tree(tree(X1, X2, X3), X4, X5), tree(tree(X6, X7, X8), X9, X10)) → U8_GA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, balancecA_in_gagaaaaaaa(X1, X11, X2, X12, .(','(X10, -(X13, [])), .(','(X6, -(X11, .(X7, X14))), .(','(X8, -(X14, .(X9, X13))), X15))), X15, X16, X17, X18, X19))
U8_GA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, balancecA_out_gagaaaaaaa(X1, X11, X2, X12, .(','(X10, -(X13, [])), .(','(X6, -(X11, .(X7, X14))), .(','(X8, -(X14, .(X9, X13))), X15))), X15, X16, X17, X18, X19)) → U9_GA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, balanceA_in_gagaaaaaaa(X3, X12, X4, X20, X16, X17, X21, X22, X19, X23))
U8_GA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, balancecA_out_gagaaaaaaa(X1, X11, X2, X12, .(','(X10, -(X13, [])), .(','(X6, -(X11, .(X7, X14))), .(','(X8, -(X14, .(X9, X13))), X15))), X15, X16, X17, X18, X19)) → BALANCEA_IN_GAGAAAAAAA(X3, X12, X4, X20, X16, X17, X21, X22, X19, X23)
BALANCED_IN_GA(tree(X1, X2, X3), tree(X4, X5, X6)) → U10_GA(X1, X2, X3, X4, X5, X6, balancecC_in_gagaaaaaaaaaa(X1, X7, X2, X8, X4, X5, X9, X6, X10, X11, X12, X13, X14))
U10_GA(X1, X2, X3, X4, X5, X6, balancecC_out_gagaaaaaaaaaa(X1, X7, X2, X8, X4, X5, X9, X6, X10, X11, X12, X13, X14)) → U11_GA(X1, X2, X3, X4, X5, X6, balanceB_in_gaaaaa(X3, X8, X11, X12, X13, X14))
U10_GA(X1, X2, X3, X4, X5, X6, balancecC_out_gagaaaaaaaaaa(X1, X7, X2, X8, X4, X5, X9, X6, X10, X11, X12, X13, X14)) → BALANCEB_IN_GAAAAA(X3, X8, X11, X12, X13, X14)
BALANCEB_IN_GAAAAA(tree(X1, X2, X3), X4, .(','(tree(X5, X6, X7), -(X8, X9)), X10), .(','(X5, -(X8, .(X6, X11))), .(','(X7, -(X11, X9)), X12)), X13, X14) → U4_GAAAAA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, balanceA_in_gagaaaaaaa(X1, X4, X2, X15, X10, X12, X16, X17, X14, X18))
BALANCEB_IN_GAAAAA(tree(X1, X2, X3), X4, .(','(tree(X5, X6, X7), -(X8, X9)), X10), .(','(X5, -(X8, .(X6, X11))), .(','(X7, -(X11, X9)), X12)), X13, X14) → BALANCEA_IN_GAGAAAAAAA(X1, X4, X2, X15, X10, X12, X16, X17, X14, X18)
BALANCEB_IN_GAAAAA(tree(X1, X2, X3), X4, .(','(tree(X5, X6, X7), -(X8, X9)), X10), .(','(X5, -(X8, .(X6, X11))), .(','(X7, -(X11, X9)), X12)), X13, X14) → U5_GAAAAA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, balancecA_in_gagaaaaaaa(X1, X4, X2, X15, X10, X12, X16, X17, X14, X18))
U5_GAAAAA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, balancecA_out_gagaaaaaaa(X1, X4, X2, X15, X10, X12, X16, X17, X14, X18)) → U6_GAAAAA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, balanceB_in_gaaaaa(X3, X15, X16, X17, X13, X18))
U5_GAAAAA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, balancecA_out_gagaaaaaaa(X1, X4, X2, X15, X10, X12, X16, X17, X14, X18)) → BALANCEB_IN_GAAAAA(X3, X15, X16, X17, X13, X18)

The TRS R consists of the following rules:

balancecA_in_gagaaaaaaa(nil, .(X1, X2), X1, X2, X3, X4, X3, X4, .(','(nil, -(X5, X5)), X6), X6) → balancecA_out_gagaaaaaaa(nil, .(X1, X2), X1, X2, X3, X4, X3, X4, .(','(nil, -(X5, X5)), X6), X6)
balancecA_in_gagaaaaaaa(tree(X1, X2, X3), X4, X5, X6, .(','(tree(X7, X8, X9), -(X10, X11)), X12), .(','(X7, -(X10, .(X8, X13))), .(','(X9, -(X13, X11)), X14)), X15, X16, X17, X18) → U13_gagaaaaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, balancecA_in_gagaaaaaaa(X1, X4, X2, X19, X12, X14, X20, X21, X17, X22))
U13_gagaaaaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, balancecA_out_gagaaaaaaa(X1, X4, X2, X19, X12, X14, X20, X21, X17, X22)) → U14_gagaaaaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, balancecA_in_gagaaaaaaa(X3, X19, X5, X6, X20, X21, X15, X16, X22, X18))
U14_gagaaaaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, balancecA_out_gagaaaaaaa(X3, X19, X5, X6, X20, X21, X15, X16, X22, X18)) → balancecA_out_gagaaaaaaa(tree(X1, X2, X3), X4, X5, X6, .(','(tree(X7, X8, X9), -(X10, X11)), X12), .(','(X7, -(X10, .(X8, X13))), .(','(X9, -(X13, X11)), X14)), X15, X16, X17, X18)
balancecC_in_gagaaaaaaaaaa(nil, .(X1, X2), X1, X2, X3, X4, X5, X6, X7, .(','(X3, -(.(X1, X2), .(X4, X5))), .(','(X6, -(X5, [])), X7)), X7, .(','(nil, -(X8, X8)), X9), X9) → balancecC_out_gagaaaaaaaaaa(nil, .(X1, X2), X1, X2, X3, X4, X5, X6, X7, .(','(X3, -(.(X1, X2), .(X4, X5))), .(','(X6, -(X5, [])), X7)), X7, .(','(nil, -(X8, X8)), X9), X9)
balancecC_in_gagaaaaaaaaaa(tree(X1, X2, X3), X4, X5, X6, tree(X7, X8, X9), X10, X11, X12, .(','(X7, -(X4, .(X8, X13))), .(','(X9, -(X13, .(X10, X11))), X14)), X15, X16, X17, X18) → U17_gagaaaaaaaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, balancecA_in_gagaaaaaaa(X1, X4, X2, X19, .(','(X12, -(X11, [])), .(','(X7, -(X4, .(X8, X13))), .(','(X9, -(X13, .(X10, X11))), X14))), X14, X20, X21, X17, X22))
U17_gagaaaaaaaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, balancecA_out_gagaaaaaaa(X1, X4, X2, X19, .(','(X12, -(X11, [])), .(','(X7, -(X4, .(X8, X13))), .(','(X9, -(X13, .(X10, X11))), X14))), X14, X20, X21, X17, X22)) → U18_gagaaaaaaaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, balancecA_in_gagaaaaaaa(X3, X19, X5, X6, X20, X21, X15, X16, X22, X18))
U18_gagaaaaaaaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, balancecA_out_gagaaaaaaa(X3, X19, X5, X6, X20, X21, X15, X16, X22, X18)) → balancecC_out_gagaaaaaaaaaa(tree(X1, X2, X3), X4, X5, X6, tree(X7, X8, X9), X10, X11, X12, .(','(X7, -(X4, .(X8, X13))), .(','(X9, -(X13, .(X10, X11))), X14)), X15, X16, X17, X18)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
balanceA_in_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balanceA_in_gagaaaaaaa(x1, x3)
balancecA_in_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balancecA_in_gagaaaaaaa(x1, x3)
nil  =  nil
balancecA_out_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balancecA_out_gagaaaaaaa(x1, x3)
U13_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U13_gagaaaaaaa(x1, x2, x3, x5, x19)
U14_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23)  =  U14_gagaaaaaaa(x1, x2, x3, x5, x23)
balancecC_in_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  balancecC_in_gagaaaaaaaaaa(x1, x3)
balancecC_out_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  balancecC_out_gagaaaaaaaaaa(x1, x3)
U17_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U17_gagaaaaaaaaaa(x1, x2, x3, x5, x19)
U18_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23)  =  U18_gagaaaaaaaaaa(x1, x2, x3, x5, x23)
balanceB_in_gaaaaa(x1, x2, x3, x4, x5, x6)  =  balanceB_in_gaaaaa(x1)
BALANCED_IN_GA(x1, x2)  =  BALANCED_IN_GA(x1)
U7_GA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U7_GA(x1, x2, x3, x4, x5, x11)
BALANCEA_IN_GAGAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  BALANCEA_IN_GAGAAAAAAA(x1, x3)
U1_GAGAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U1_GAGAAAAAAA(x1, x2, x3, x5, x19)
U2_GAGAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U2_GAGAAAAAAA(x1, x2, x3, x5, x19)
U3_GAGAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U3_GAGAAAAAAA(x1, x2, x3, x5, x19)
U8_GA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U8_GA(x1, x2, x3, x4, x5, x11)
U9_GA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U9_GA(x1, x2, x3, x4, x5, x11)
U10_GA(x1, x2, x3, x4, x5, x6, x7)  =  U10_GA(x1, x2, x3, x7)
U11_GA(x1, x2, x3, x4, x5, x6, x7)  =  U11_GA(x1, x2, x3, x7)
BALANCEB_IN_GAAAAA(x1, x2, x3, x4, x5, x6)  =  BALANCEB_IN_GAAAAA(x1)
U4_GAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)  =  U4_GAAAAA(x1, x2, x3, x15)
U5_GAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)  =  U5_GAAAAA(x1, x2, x3, x15)
U6_GAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)  =  U6_GAAAAA(x1, x2, x3, x15)

We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 13 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

BALANCEA_IN_GAGAAAAAAA(tree(X1, X2, X3), X4, X5, X6, .(','(tree(X7, X8, X9), -(X10, X11)), X12), .(','(X7, -(X10, .(X8, X13))), .(','(X9, -(X13, X11)), X14)), X15, X16, X17, X18) → U2_GAGAAAAAAA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, balancecA_in_gagaaaaaaa(X1, X4, X2, X19, X12, X14, X20, X21, X17, X22))
U2_GAGAAAAAAA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, balancecA_out_gagaaaaaaa(X1, X4, X2, X19, X12, X14, X20, X21, X17, X22)) → BALANCEA_IN_GAGAAAAAAA(X3, X19, X5, X6, X20, X21, X15, X16, X22, X18)
BALANCEA_IN_GAGAAAAAAA(tree(X1, X2, X3), X4, X5, X6, .(','(tree(X7, X8, X9), -(X10, X11)), X12), .(','(X7, -(X10, .(X8, X13))), .(','(X9, -(X13, X11)), X14)), X15, X16, X17, X18) → BALANCEA_IN_GAGAAAAAAA(X1, X4, X2, X19, X12, X14, X20, X21, X17, X22)

The TRS R consists of the following rules:

balancecA_in_gagaaaaaaa(nil, .(X1, X2), X1, X2, X3, X4, X3, X4, .(','(nil, -(X5, X5)), X6), X6) → balancecA_out_gagaaaaaaa(nil, .(X1, X2), X1, X2, X3, X4, X3, X4, .(','(nil, -(X5, X5)), X6), X6)
balancecA_in_gagaaaaaaa(tree(X1, X2, X3), X4, X5, X6, .(','(tree(X7, X8, X9), -(X10, X11)), X12), .(','(X7, -(X10, .(X8, X13))), .(','(X9, -(X13, X11)), X14)), X15, X16, X17, X18) → U13_gagaaaaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, balancecA_in_gagaaaaaaa(X1, X4, X2, X19, X12, X14, X20, X21, X17, X22))
U13_gagaaaaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, balancecA_out_gagaaaaaaa(X1, X4, X2, X19, X12, X14, X20, X21, X17, X22)) → U14_gagaaaaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, balancecA_in_gagaaaaaaa(X3, X19, X5, X6, X20, X21, X15, X16, X22, X18))
U14_gagaaaaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, balancecA_out_gagaaaaaaa(X3, X19, X5, X6, X20, X21, X15, X16, X22, X18)) → balancecA_out_gagaaaaaaa(tree(X1, X2, X3), X4, X5, X6, .(','(tree(X7, X8, X9), -(X10, X11)), X12), .(','(X7, -(X10, .(X8, X13))), .(','(X9, -(X13, X11)), X14)), X15, X16, X17, X18)
balancecC_in_gagaaaaaaaaaa(nil, .(X1, X2), X1, X2, X3, X4, X5, X6, X7, .(','(X3, -(.(X1, X2), .(X4, X5))), .(','(X6, -(X5, [])), X7)), X7, .(','(nil, -(X8, X8)), X9), X9) → balancecC_out_gagaaaaaaaaaa(nil, .(X1, X2), X1, X2, X3, X4, X5, X6, X7, .(','(X3, -(.(X1, X2), .(X4, X5))), .(','(X6, -(X5, [])), X7)), X7, .(','(nil, -(X8, X8)), X9), X9)
balancecC_in_gagaaaaaaaaaa(tree(X1, X2, X3), X4, X5, X6, tree(X7, X8, X9), X10, X11, X12, .(','(X7, -(X4, .(X8, X13))), .(','(X9, -(X13, .(X10, X11))), X14)), X15, X16, X17, X18) → U17_gagaaaaaaaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, balancecA_in_gagaaaaaaa(X1, X4, X2, X19, .(','(X12, -(X11, [])), .(','(X7, -(X4, .(X8, X13))), .(','(X9, -(X13, .(X10, X11))), X14))), X14, X20, X21, X17, X22))
U17_gagaaaaaaaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, balancecA_out_gagaaaaaaa(X1, X4, X2, X19, .(','(X12, -(X11, [])), .(','(X7, -(X4, .(X8, X13))), .(','(X9, -(X13, .(X10, X11))), X14))), X14, X20, X21, X17, X22)) → U18_gagaaaaaaaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, balancecA_in_gagaaaaaaa(X3, X19, X5, X6, X20, X21, X15, X16, X22, X18))
U18_gagaaaaaaaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, balancecA_out_gagaaaaaaa(X3, X19, X5, X6, X20, X21, X15, X16, X22, X18)) → balancecC_out_gagaaaaaaaaaa(tree(X1, X2, X3), X4, X5, X6, tree(X7, X8, X9), X10, X11, X12, .(','(X7, -(X4, .(X8, X13))), .(','(X9, -(X13, .(X10, X11))), X14)), X15, X16, X17, X18)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
balancecA_in_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balancecA_in_gagaaaaaaa(x1, x3)
nil  =  nil
balancecA_out_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balancecA_out_gagaaaaaaa(x1, x3)
U13_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U13_gagaaaaaaa(x1, x2, x3, x5, x19)
U14_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23)  =  U14_gagaaaaaaa(x1, x2, x3, x5, x23)
balancecC_in_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  balancecC_in_gagaaaaaaaaaa(x1, x3)
balancecC_out_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  balancecC_out_gagaaaaaaaaaa(x1, x3)
U17_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U17_gagaaaaaaaaaa(x1, x2, x3, x5, x19)
U18_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23)  =  U18_gagaaaaaaaaaa(x1, x2, x3, x5, x23)
BALANCEA_IN_GAGAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  BALANCEA_IN_GAGAAAAAAA(x1, x3)
U2_GAGAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U2_GAGAAAAAAA(x1, x2, x3, x5, x19)

We have to consider all (P,R,Pi)-chains

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

BALANCEA_IN_GAGAAAAAAA(tree(X1, X2, X3), X4, X5, X6, .(','(tree(X7, X8, X9), -(X10, X11)), X12), .(','(X7, -(X10, .(X8, X13))), .(','(X9, -(X13, X11)), X14)), X15, X16, X17, X18) → U2_GAGAAAAAAA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, balancecA_in_gagaaaaaaa(X1, X4, X2, X19, X12, X14, X20, X21, X17, X22))
U2_GAGAAAAAAA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, balancecA_out_gagaaaaaaa(X1, X4, X2, X19, X12, X14, X20, X21, X17, X22)) → BALANCEA_IN_GAGAAAAAAA(X3, X19, X5, X6, X20, X21, X15, X16, X22, X18)
BALANCEA_IN_GAGAAAAAAA(tree(X1, X2, X3), X4, X5, X6, .(','(tree(X7, X8, X9), -(X10, X11)), X12), .(','(X7, -(X10, .(X8, X13))), .(','(X9, -(X13, X11)), X14)), X15, X16, X17, X18) → BALANCEA_IN_GAGAAAAAAA(X1, X4, X2, X19, X12, X14, X20, X21, X17, X22)

The TRS R consists of the following rules:

balancecA_in_gagaaaaaaa(nil, .(X1, X2), X1, X2, X3, X4, X3, X4, .(','(nil, -(X5, X5)), X6), X6) → balancecA_out_gagaaaaaaa(nil, .(X1, X2), X1, X2, X3, X4, X3, X4, .(','(nil, -(X5, X5)), X6), X6)
balancecA_in_gagaaaaaaa(tree(X1, X2, X3), X4, X5, X6, .(','(tree(X7, X8, X9), -(X10, X11)), X12), .(','(X7, -(X10, .(X8, X13))), .(','(X9, -(X13, X11)), X14)), X15, X16, X17, X18) → U13_gagaaaaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, balancecA_in_gagaaaaaaa(X1, X4, X2, X19, X12, X14, X20, X21, X17, X22))
U13_gagaaaaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, balancecA_out_gagaaaaaaa(X1, X4, X2, X19, X12, X14, X20, X21, X17, X22)) → U14_gagaaaaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, balancecA_in_gagaaaaaaa(X3, X19, X5, X6, X20, X21, X15, X16, X22, X18))
U14_gagaaaaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, balancecA_out_gagaaaaaaa(X3, X19, X5, X6, X20, X21, X15, X16, X22, X18)) → balancecA_out_gagaaaaaaa(tree(X1, X2, X3), X4, X5, X6, .(','(tree(X7, X8, X9), -(X10, X11)), X12), .(','(X7, -(X10, .(X8, X13))), .(','(X9, -(X13, X11)), X14)), X15, X16, X17, X18)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
balancecA_in_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balancecA_in_gagaaaaaaa(x1, x3)
nil  =  nil
balancecA_out_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balancecA_out_gagaaaaaaa(x1, x3)
U13_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U13_gagaaaaaaa(x1, x2, x3, x5, x19)
U14_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23)  =  U14_gagaaaaaaa(x1, x2, x3, x5, x23)
BALANCEA_IN_GAGAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  BALANCEA_IN_GAGAAAAAAA(x1, x3)
U2_GAGAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U2_GAGAAAAAAA(x1, x2, x3, x5, x19)

We have to consider all (P,R,Pi)-chains

(10) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

BALANCEA_IN_GAGAAAAAAA(tree(X1, X2, X3), X5) → U2_GAGAAAAAAA(X1, X2, X3, X5, balancecA_in_gagaaaaaaa(X1, X2))
U2_GAGAAAAAAA(X1, X2, X3, X5, balancecA_out_gagaaaaaaa(X1, X2)) → BALANCEA_IN_GAGAAAAAAA(X3, X5)
BALANCEA_IN_GAGAAAAAAA(tree(X1, X2, X3), X5) → BALANCEA_IN_GAGAAAAAAA(X1, X2)

The TRS R consists of the following rules:

balancecA_in_gagaaaaaaa(nil, X1) → balancecA_out_gagaaaaaaa(nil, X1)
balancecA_in_gagaaaaaaa(tree(X1, X2, X3), X5) → U13_gagaaaaaaa(X1, X2, X3, X5, balancecA_in_gagaaaaaaa(X1, X2))
U13_gagaaaaaaa(X1, X2, X3, X5, balancecA_out_gagaaaaaaa(X1, X2)) → U14_gagaaaaaaa(X1, X2, X3, X5, balancecA_in_gagaaaaaaa(X3, X5))
U14_gagaaaaaaa(X1, X2, X3, X5, balancecA_out_gagaaaaaaa(X3, X5)) → balancecA_out_gagaaaaaaa(tree(X1, X2, X3), X5)

The set Q consists of the following terms:

balancecA_in_gagaaaaaaa(x0, x1)
U13_gagaaaaaaa(x0, x1, x2, x3, x4)
U14_gagaaaaaaa(x0, x1, x2, x3, x4)

We have to consider all (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• U2_GAGAAAAAAA(X1, X2, X3, X5, balancecA_out_gagaaaaaaa(X1, X2)) → BALANCEA_IN_GAGAAAAAAA(X3, X5)
  The graph contains the following edges 3 >= 1, 4 >= 2

• BALANCEA_IN_GAGAAAAAAA(tree(X1, X2, X3), X5) → BALANCEA_IN_GAGAAAAAAA(X1, X2)
  The graph contains the following edges 1 > 1, 1 > 2

• BALANCEA_IN_GAGAAAAAAA(tree(X1, X2, X3), X5) → U2_GAGAAAAAAA(X1, X2, X3, X5, balancecA_in_gagaaaaaaa(X1, X2))
  The graph contains the following edges 1 > 1, 1 > 2, 1 > 3, 2 >= 4

(13) YES

(14) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

BALANCEB_IN_GAAAAA(tree(X1, X2, X3), X4, .(','(tree(X5, X6, X7), -(X8, X9)), X10), .(','(X5, -(X8, .(X6, X11))), .(','(X7, -(X11, X9)), X12)), X13, X14) → U5_GAAAAA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, balancecA_in_gagaaaaaaa(X1, X4, X2, X15, X10, X12, X16, X17, X14, X18))
U5_GAAAAA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, balancecA_out_gagaaaaaaa(X1, X4, X2, X15, X10, X12, X16, X17, X14, X18)) → BALANCEB_IN_GAAAAA(X3, X15, X16, X17, X13, X18)

The TRS R consists of the following rules:

balancecA_in_gagaaaaaaa(nil, .(X1, X2), X1, X2, X3, X4, X3, X4, .(','(nil, -(X5, X5)), X6), X6) → balancecA_out_gagaaaaaaa(nil, .(X1, X2), X1, X2, X3, X4, X3, X4, .(','(nil, -(X5, X5)), X6), X6)
balancecA_in_gagaaaaaaa(tree(X1, X2, X3), X4, X5, X6, .(','(tree(X7, X8, X9), -(X10, X11)), X12), .(','(X7, -(X10, .(X8, X13))), .(','(X9, -(X13, X11)), X14)), X15, X16, X17, X18) → U13_gagaaaaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, balancecA_in_gagaaaaaaa(X1, X4, X2, X19, X12, X14, X20, X21, X17, X22))
U13_gagaaaaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, balancecA_out_gagaaaaaaa(X1, X4, X2, X19, X12, X14, X20, X21, X17, X22)) → U14_gagaaaaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, balancecA_in_gagaaaaaaa(X3, X19, X5, X6, X20, X21, X15, X16, X22, X18))
U14_gagaaaaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, balancecA_out_gagaaaaaaa(X3, X19, X5, X6, X20, X21, X15, X16, X22, X18)) → balancecA_out_gagaaaaaaa(tree(X1, X2, X3), X4, X5, X6, .(','(tree(X7, X8, X9), -(X10, X11)), X12), .(','(X7, -(X10, .(X8, X13))), .(','(X9, -(X13, X11)), X14)), X15, X16, X17, X18)
balancecC_in_gagaaaaaaaaaa(nil, .(X1, X2), X1, X2, X3, X4, X5, X6, X7, .(','(X3, -(.(X1, X2), .(X4, X5))), .(','(X6, -(X5, [])), X7)), X7, .(','(nil, -(X8, X8)), X9), X9) → balancecC_out_gagaaaaaaaaaa(nil, .(X1, X2), X1, X2, X3, X4, X5, X6, X7, .(','(X3, -(.(X1, X2), .(X4, X5))), .(','(X6, -(X5, [])), X7)), X7, .(','(nil, -(X8, X8)), X9), X9)
balancecC_in_gagaaaaaaaaaa(tree(X1, X2, X3), X4, X5, X6, tree(X7, X8, X9), X10, X11, X12, .(','(X7, -(X4, .(X8, X13))), .(','(X9, -(X13, .(X10, X11))), X14)), X15, X16, X17, X18) → U17_gagaaaaaaaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, balancecA_in_gagaaaaaaa(X1, X4, X2, X19, .(','(X12, -(X11, [])), .(','(X7, -(X4, .(X8, X13))), .(','(X9, -(X13, .(X10, X11))), X14))), X14, X20, X21, X17, X22))
U17_gagaaaaaaaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, balancecA_out_gagaaaaaaa(X1, X4, X2, X19, .(','(X12, -(X11, [])), .(','(X7, -(X4, .(X8, X13))), .(','(X9, -(X13, .(X10, X11))), X14))), X14, X20, X21, X17, X22)) → U18_gagaaaaaaaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, balancecA_in_gagaaaaaaa(X3, X19, X5, X6, X20, X21, X15, X16, X22, X18))
U18_gagaaaaaaaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, balancecA_out_gagaaaaaaa(X3, X19, X5, X6, X20, X21, X15, X16, X22, X18)) → balancecC_out_gagaaaaaaaaaa(tree(X1, X2, X3), X4, X5, X6, tree(X7, X8, X9), X10, X11, X12, .(','(X7, -(X4, .(X8, X13))), .(','(X9, -(X13, .(X10, X11))), X14)), X15, X16, X17, X18)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
balancecA_in_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balancecA_in_gagaaaaaaa(x1, x3)
nil  =  nil
balancecA_out_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balancecA_out_gagaaaaaaa(x1, x3)
U13_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U13_gagaaaaaaa(x1, x2, x3, x5, x19)
U14_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23)  =  U14_gagaaaaaaa(x1, x2, x3, x5, x23)
balancecC_in_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  balancecC_in_gagaaaaaaaaaa(x1, x3)
balancecC_out_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)  =  balancecC_out_gagaaaaaaaaaa(x1, x3)
U17_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U17_gagaaaaaaaaaa(x1, x2, x3, x5, x19)
U18_gagaaaaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23)  =  U18_gagaaaaaaaaaa(x1, x2, x3, x5, x23)
BALANCEB_IN_GAAAAA(x1, x2, x3, x4, x5, x6)  =  BALANCEB_IN_GAAAAA(x1)
U5_GAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)  =  U5_GAAAAA(x1, x2, x3, x15)

We have to consider all (P,R,Pi)-chains

(15) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

BALANCEB_IN_GAAAAA(tree(X1, X2, X3), X4, .(','(tree(X5, X6, X7), -(X8, X9)), X10), .(','(X5, -(X8, .(X6, X11))), .(','(X7, -(X11, X9)), X12)), X13, X14) → U5_GAAAAA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, balancecA_in_gagaaaaaaa(X1, X4, X2, X15, X10, X12, X16, X17, X14, X18))
U5_GAAAAA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, balancecA_out_gagaaaaaaa(X1, X4, X2, X15, X10, X12, X16, X17, X14, X18)) → BALANCEB_IN_GAAAAA(X3, X15, X16, X17, X13, X18)

The TRS R consists of the following rules:

balancecA_in_gagaaaaaaa(nil, .(X1, X2), X1, X2, X3, X4, X3, X4, .(','(nil, -(X5, X5)), X6), X6) → balancecA_out_gagaaaaaaa(nil, .(X1, X2), X1, X2, X3, X4, X3, X4, .(','(nil, -(X5, X5)), X6), X6)
balancecA_in_gagaaaaaaa(tree(X1, X2, X3), X4, X5, X6, .(','(tree(X7, X8, X9), -(X10, X11)), X12), .(','(X7, -(X10, .(X8, X13))), .(','(X9, -(X13, X11)), X14)), X15, X16, X17, X18) → U13_gagaaaaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, balancecA_in_gagaaaaaaa(X1, X4, X2, X19, X12, X14, X20, X21, X17, X22))
U13_gagaaaaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, balancecA_out_gagaaaaaaa(X1, X4, X2, X19, X12, X14, X20, X21, X17, X22)) → U14_gagaaaaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, balancecA_in_gagaaaaaaa(X3, X19, X5, X6, X20, X21, X15, X16, X22, X18))
U14_gagaaaaaaa(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, balancecA_out_gagaaaaaaa(X3, X19, X5, X6, X20, X21, X15, X16, X22, X18)) → balancecA_out_gagaaaaaaa(tree(X1, X2, X3), X4, X5, X6, .(','(tree(X7, X8, X9), -(X10, X11)), X12), .(','(X7, -(X10, .(X8, X13))), .(','(X9, -(X13, X11)), X14)), X15, X16, X17, X18)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
balancecA_in_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balancecA_in_gagaaaaaaa(x1, x3)
nil  =  nil
balancecA_out_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  balancecA_out_gagaaaaaaa(x1, x3)
U13_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19)  =  U13_gagaaaaaaa(x1, x2, x3, x5, x19)
U14_gagaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23)  =  U14_gagaaaaaaa(x1, x2, x3, x5, x23)
BALANCEB_IN_GAAAAA(x1, x2, x3, x4, x5, x6)  =  BALANCEB_IN_GAAAAA(x1)
U5_GAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)  =  U5_GAAAAA(x1, x2, x3, x15)

We have to consider all (P,R,Pi)-chains

(17) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

BALANCEB_IN_GAAAAA(tree(X1, X2, X3)) → U5_GAAAAA(X1, X2, X3, balancecA_in_gagaaaaaaa(X1, X2))
U5_GAAAAA(X1, X2, X3, balancecA_out_gagaaaaaaa(X1, X2)) → BALANCEB_IN_GAAAAA(X3)

The TRS R consists of the following rules:

balancecA_in_gagaaaaaaa(nil, X1) → balancecA_out_gagaaaaaaa(nil, X1)
balancecA_in_gagaaaaaaa(tree(X1, X2, X3), X5) → U13_gagaaaaaaa(X1, X2, X3, X5, balancecA_in_gagaaaaaaa(X1, X2))
U13_gagaaaaaaa(X1, X2, X3, X5, balancecA_out_gagaaaaaaa(X1, X2)) → U14_gagaaaaaaa(X1, X2, X3, X5, balancecA_in_gagaaaaaaa(X3, X5))
U14_gagaaaaaaa(X1, X2, X3, X5, balancecA_out_gagaaaaaaa(X3, X5)) → balancecA_out_gagaaaaaaa(tree(X1, X2, X3), X5)

The set Q consists of the following terms:

balancecA_in_gagaaaaaaa(x0, x1)
U13_gagaaaaaaa(x0, x1, x2, x3, x4)
U14_gagaaaaaaa(x0, x1, x2, x3, x4)

We have to consider all (P,Q,R)-chains.

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• U5_GAAAAA(X1, X2, X3, balancecA_out_gagaaaaaaa(X1, X2)) → BALANCEB_IN_GAAAAA(X3)
  The graph contains the following edges 3 >= 1

• BALANCEB_IN_GAAAAA(tree(X1, X2, X3)) → U5_GAAAAA(X1, X2, X3, balancecA_in_gagaaaaaaa(X1, X2))
  The graph contains the following edges 1 > 1, 1 > 2, 1 > 3

(20) YES